<HEAD><TITLE>Hindley-Milner Type Inference</TITLE>
<META http-equiv="Content-Style-Type" content="text/css" />
<META http-equiv="content-type" content="text/html; charset=utf-8" />  
<STYLE type="text/css">
 body {
    font-family: Helvetica, Sans;
 }
 pre.code {
        margin: 15px;
       background-color: #FFFFFF;
       font-family: Courier,Courier New, Fixed;
       font-weight: Bold;
       font-size: 14px;
}
span.Red1 {color: rgb(212,0,0);}
span.Red2 {color: rgb(253,51,1);}
span.Red3 {color: rgb(244,72,0);}
span.Blue1 {color: rgb(0,136,170);}
span.Blue2 {color: rgb(0,102,128);}
span.Blue3 {color: rgb(0,51,153);}
span.Purple1 {color: rgb(180,120,204);}
span.Purple2 {color: rgb(156,72,184);}
span.Purple3 {color: rgb(100,0,136);}
span.Yellow1 {color: rgb(240,236,4);}
span.Yellow2 {color: rgb(224,212,12);}
span.Yellow3 {color: rgb(184,160,28);}
span.Brown1 {color: rgb(238,199,62);}
span.Brown2 {color: rgb(204,102,51);}
span.Brown3 {color: rgb(152,102,1);}
span.Orange1 {color: rgb(255,102,51);}
span.Orange2 {color: rgb(255,153,51);}
span.Orange3 {color: rgb(255,204,0);}
span.Grey1 {color: rgb(153,153,153);}
span.Grey2 {color: rgb(128,128,128);}
span.Grey3 {color: rgb(102,102,102);}
span.Grey4 {color: rgb(51,51,51);}
span.Green1 {color: rgb(102,204,0);}
span.Green2 {color: rgb(102,204,102);}
span.Green3 {color: rgb(51,153,102);}
</STYLE>
</HEAD>
<BODY>
<H1>Hindley-Milner Type Inference</H1>
<P>Robin Milner's type system with parametric polymorphism was a
significant advance over the systems of Russell and Church. Arguably
it is the ability to use type-variables that makes higher order logic
a practical vehicle for proving non-trivial theorems. The
Hindley-Milner algorithm is used to automatically infer types in
theorem provers and in several other functional programing languages.

<P>The algorithm, the type system, and some of the logical background are explained
in <a href="hindley-milner.pdf">this tutorial</a>, along with an implementation
in standard ML.
<P align="center"><IMG SRC="hm.png">
<P>This implementation is purely functional and is intended to show
the algorithm as clearly as possible. The image above is meant to show
that functional languages can be used to express mathematics and logic
in such a way that the correspondence between the mathematical and the
programmatic expressions may be as exact as one wishes. 

<P>This has practical consequences. In implementing the algorithm in
ML I found several errors and ambiguities in the mathematical
expression. These were cleared up in the process of constructing the
mechanical expression of the algorithm. The errors would have been
detected by the syntax and type-checking of the compiler, and the
ambiguity is resolved by the specification of standard ML semantics
which is more precise than any informal description of mathematical
notation that I have ever seen. Because ML is equally expressive but
more exact, I argue that the ML program is a a <I>better</I>
description of the algorithm than the mathematical one.

<P>Standard ML is Milner's language which uses this parametric
polymorphic type system. The core of the implementation of the type
inference algorithm consists in some 250 lines of code. It does not
include any explicit type annotation at all, yet the type of each and
every expression is inferred (and thereby checked) by the same
algorithm which is part of the compiler.

<P>The algorithm was proved sound and complete by Damas and Milner in
1982 and the proof is outlined in <a href="milner-damas.pdf">Principal
type-schemes for functional programs</a> which I have re-keyed because
the paper is so well-written and deserves to be more widely read.

<P>The source code is available
as a <a href="hindley-milner.txt">plain text SML source file</a> and
as <a href="hindley-milner.html">html formatted standard ML</a>.

</BODY>
</HTML>
